0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 88 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 27 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 10 ms)
↳20 QDP
↳21 MRRProof (⇔, 24 ms)
↳22 QDP
↳23 PisEmptyProof (⇔, 0 ms)
↳24 YES
permuteB_in_ga([], []) → permuteB_out_ga([], [])
permuteB_in_ga(.(T21, T22), .(T21, T23)) → U2_ga(T21, T22, T23, permuteB_in_ga(T22, T23))
permuteB_in_ga(.(T37, T38), .(T39, T40)) → U3_ga(T37, T38, T39, T40, deleteA_in_aga(T39, T38, X42))
deleteA_in_aga(T59, .(T59, T60), T60) → deleteA_out_aga(T59, .(T59, T60), T60)
deleteA_in_aga(T70, .(T68, T69), .(T68, X75)) → U1_aga(T70, T68, T69, X75, deleteA_in_aga(T70, T69, X75))
U1_aga(T70, T68, T69, X75, deleteA_out_aga(T70, T69, X75)) → deleteA_out_aga(T70, .(T68, T69), .(T68, X75))
U3_ga(T37, T38, T39, T40, deleteA_out_aga(T39, T38, X42)) → permuteB_out_ga(.(T37, T38), .(T39, T40))
permuteB_in_ga(.(T37, T38), .(T39, T46)) → U4_ga(T37, T38, T39, T46, deleteA_in_aga(T39, T38, T45))
U4_ga(T37, T38, T39, T46, deleteA_out_aga(T39, T38, T45)) → U5_ga(T37, T38, T39, T46, permuteB_in_ga(.(T37, T45), T46))
U5_ga(T37, T38, T39, T46, permuteB_out_ga(.(T37, T45), T46)) → permuteB_out_ga(.(T37, T38), .(T39, T46))
U2_ga(T21, T22, T23, permuteB_out_ga(T22, T23)) → permuteB_out_ga(.(T21, T22), .(T21, T23))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
permuteB_in_ga([], []) → permuteB_out_ga([], [])
permuteB_in_ga(.(T21, T22), .(T21, T23)) → U2_ga(T21, T22, T23, permuteB_in_ga(T22, T23))
permuteB_in_ga(.(T37, T38), .(T39, T40)) → U3_ga(T37, T38, T39, T40, deleteA_in_aga(T39, T38, X42))
deleteA_in_aga(T59, .(T59, T60), T60) → deleteA_out_aga(T59, .(T59, T60), T60)
deleteA_in_aga(T70, .(T68, T69), .(T68, X75)) → U1_aga(T70, T68, T69, X75, deleteA_in_aga(T70, T69, X75))
U1_aga(T70, T68, T69, X75, deleteA_out_aga(T70, T69, X75)) → deleteA_out_aga(T70, .(T68, T69), .(T68, X75))
U3_ga(T37, T38, T39, T40, deleteA_out_aga(T39, T38, X42)) → permuteB_out_ga(.(T37, T38), .(T39, T40))
permuteB_in_ga(.(T37, T38), .(T39, T46)) → U4_ga(T37, T38, T39, T46, deleteA_in_aga(T39, T38, T45))
U4_ga(T37, T38, T39, T46, deleteA_out_aga(T39, T38, T45)) → U5_ga(T37, T38, T39, T46, permuteB_in_ga(.(T37, T45), T46))
U5_ga(T37, T38, T39, T46, permuteB_out_ga(.(T37, T45), T46)) → permuteB_out_ga(.(T37, T38), .(T39, T46))
U2_ga(T21, T22, T23, permuteB_out_ga(T22, T23)) → permuteB_out_ga(.(T21, T22), .(T21, T23))
PERMUTEB_IN_GA(.(T21, T22), .(T21, T23)) → U2_GA(T21, T22, T23, permuteB_in_ga(T22, T23))
PERMUTEB_IN_GA(.(T21, T22), .(T21, T23)) → PERMUTEB_IN_GA(T22, T23)
PERMUTEB_IN_GA(.(T37, T38), .(T39, T40)) → U3_GA(T37, T38, T39, T40, deleteA_in_aga(T39, T38, X42))
PERMUTEB_IN_GA(.(T37, T38), .(T39, T40)) → DELETEA_IN_AGA(T39, T38, X42)
DELETEA_IN_AGA(T70, .(T68, T69), .(T68, X75)) → U1_AGA(T70, T68, T69, X75, deleteA_in_aga(T70, T69, X75))
DELETEA_IN_AGA(T70, .(T68, T69), .(T68, X75)) → DELETEA_IN_AGA(T70, T69, X75)
PERMUTEB_IN_GA(.(T37, T38), .(T39, T46)) → U4_GA(T37, T38, T39, T46, deleteA_in_aga(T39, T38, T45))
U4_GA(T37, T38, T39, T46, deleteA_out_aga(T39, T38, T45)) → U5_GA(T37, T38, T39, T46, permuteB_in_ga(.(T37, T45), T46))
U4_GA(T37, T38, T39, T46, deleteA_out_aga(T39, T38, T45)) → PERMUTEB_IN_GA(.(T37, T45), T46)
permuteB_in_ga([], []) → permuteB_out_ga([], [])
permuteB_in_ga(.(T21, T22), .(T21, T23)) → U2_ga(T21, T22, T23, permuteB_in_ga(T22, T23))
permuteB_in_ga(.(T37, T38), .(T39, T40)) → U3_ga(T37, T38, T39, T40, deleteA_in_aga(T39, T38, X42))
deleteA_in_aga(T59, .(T59, T60), T60) → deleteA_out_aga(T59, .(T59, T60), T60)
deleteA_in_aga(T70, .(T68, T69), .(T68, X75)) → U1_aga(T70, T68, T69, X75, deleteA_in_aga(T70, T69, X75))
U1_aga(T70, T68, T69, X75, deleteA_out_aga(T70, T69, X75)) → deleteA_out_aga(T70, .(T68, T69), .(T68, X75))
U3_ga(T37, T38, T39, T40, deleteA_out_aga(T39, T38, X42)) → permuteB_out_ga(.(T37, T38), .(T39, T40))
permuteB_in_ga(.(T37, T38), .(T39, T46)) → U4_ga(T37, T38, T39, T46, deleteA_in_aga(T39, T38, T45))
U4_ga(T37, T38, T39, T46, deleteA_out_aga(T39, T38, T45)) → U5_ga(T37, T38, T39, T46, permuteB_in_ga(.(T37, T45), T46))
U5_ga(T37, T38, T39, T46, permuteB_out_ga(.(T37, T45), T46)) → permuteB_out_ga(.(T37, T38), .(T39, T46))
U2_ga(T21, T22, T23, permuteB_out_ga(T22, T23)) → permuteB_out_ga(.(T21, T22), .(T21, T23))
PERMUTEB_IN_GA(.(T21, T22), .(T21, T23)) → U2_GA(T21, T22, T23, permuteB_in_ga(T22, T23))
PERMUTEB_IN_GA(.(T21, T22), .(T21, T23)) → PERMUTEB_IN_GA(T22, T23)
PERMUTEB_IN_GA(.(T37, T38), .(T39, T40)) → U3_GA(T37, T38, T39, T40, deleteA_in_aga(T39, T38, X42))
PERMUTEB_IN_GA(.(T37, T38), .(T39, T40)) → DELETEA_IN_AGA(T39, T38, X42)
DELETEA_IN_AGA(T70, .(T68, T69), .(T68, X75)) → U1_AGA(T70, T68, T69, X75, deleteA_in_aga(T70, T69, X75))
DELETEA_IN_AGA(T70, .(T68, T69), .(T68, X75)) → DELETEA_IN_AGA(T70, T69, X75)
PERMUTEB_IN_GA(.(T37, T38), .(T39, T46)) → U4_GA(T37, T38, T39, T46, deleteA_in_aga(T39, T38, T45))
U4_GA(T37, T38, T39, T46, deleteA_out_aga(T39, T38, T45)) → U5_GA(T37, T38, T39, T46, permuteB_in_ga(.(T37, T45), T46))
U4_GA(T37, T38, T39, T46, deleteA_out_aga(T39, T38, T45)) → PERMUTEB_IN_GA(.(T37, T45), T46)
permuteB_in_ga([], []) → permuteB_out_ga([], [])
permuteB_in_ga(.(T21, T22), .(T21, T23)) → U2_ga(T21, T22, T23, permuteB_in_ga(T22, T23))
permuteB_in_ga(.(T37, T38), .(T39, T40)) → U3_ga(T37, T38, T39, T40, deleteA_in_aga(T39, T38, X42))
deleteA_in_aga(T59, .(T59, T60), T60) → deleteA_out_aga(T59, .(T59, T60), T60)
deleteA_in_aga(T70, .(T68, T69), .(T68, X75)) → U1_aga(T70, T68, T69, X75, deleteA_in_aga(T70, T69, X75))
U1_aga(T70, T68, T69, X75, deleteA_out_aga(T70, T69, X75)) → deleteA_out_aga(T70, .(T68, T69), .(T68, X75))
U3_ga(T37, T38, T39, T40, deleteA_out_aga(T39, T38, X42)) → permuteB_out_ga(.(T37, T38), .(T39, T40))
permuteB_in_ga(.(T37, T38), .(T39, T46)) → U4_ga(T37, T38, T39, T46, deleteA_in_aga(T39, T38, T45))
U4_ga(T37, T38, T39, T46, deleteA_out_aga(T39, T38, T45)) → U5_ga(T37, T38, T39, T46, permuteB_in_ga(.(T37, T45), T46))
U5_ga(T37, T38, T39, T46, permuteB_out_ga(.(T37, T45), T46)) → permuteB_out_ga(.(T37, T38), .(T39, T46))
U2_ga(T21, T22, T23, permuteB_out_ga(T22, T23)) → permuteB_out_ga(.(T21, T22), .(T21, T23))
DELETEA_IN_AGA(T70, .(T68, T69), .(T68, X75)) → DELETEA_IN_AGA(T70, T69, X75)
permuteB_in_ga([], []) → permuteB_out_ga([], [])
permuteB_in_ga(.(T21, T22), .(T21, T23)) → U2_ga(T21, T22, T23, permuteB_in_ga(T22, T23))
permuteB_in_ga(.(T37, T38), .(T39, T40)) → U3_ga(T37, T38, T39, T40, deleteA_in_aga(T39, T38, X42))
deleteA_in_aga(T59, .(T59, T60), T60) → deleteA_out_aga(T59, .(T59, T60), T60)
deleteA_in_aga(T70, .(T68, T69), .(T68, X75)) → U1_aga(T70, T68, T69, X75, deleteA_in_aga(T70, T69, X75))
U1_aga(T70, T68, T69, X75, deleteA_out_aga(T70, T69, X75)) → deleteA_out_aga(T70, .(T68, T69), .(T68, X75))
U3_ga(T37, T38, T39, T40, deleteA_out_aga(T39, T38, X42)) → permuteB_out_ga(.(T37, T38), .(T39, T40))
permuteB_in_ga(.(T37, T38), .(T39, T46)) → U4_ga(T37, T38, T39, T46, deleteA_in_aga(T39, T38, T45))
U4_ga(T37, T38, T39, T46, deleteA_out_aga(T39, T38, T45)) → U5_ga(T37, T38, T39, T46, permuteB_in_ga(.(T37, T45), T46))
U5_ga(T37, T38, T39, T46, permuteB_out_ga(.(T37, T45), T46)) → permuteB_out_ga(.(T37, T38), .(T39, T46))
U2_ga(T21, T22, T23, permuteB_out_ga(T22, T23)) → permuteB_out_ga(.(T21, T22), .(T21, T23))
DELETEA_IN_AGA(T70, .(T68, T69), .(T68, X75)) → DELETEA_IN_AGA(T70, T69, X75)
DELETEA_IN_AGA(.(T68, T69)) → DELETEA_IN_AGA(T69)
From the DPs we obtained the following set of size-change graphs:
PERMUTEB_IN_GA(.(T37, T38), .(T39, T46)) → U4_GA(T37, T38, T39, T46, deleteA_in_aga(T39, T38, T45))
U4_GA(T37, T38, T39, T46, deleteA_out_aga(T39, T38, T45)) → PERMUTEB_IN_GA(.(T37, T45), T46)
PERMUTEB_IN_GA(.(T21, T22), .(T21, T23)) → PERMUTEB_IN_GA(T22, T23)
permuteB_in_ga([], []) → permuteB_out_ga([], [])
permuteB_in_ga(.(T21, T22), .(T21, T23)) → U2_ga(T21, T22, T23, permuteB_in_ga(T22, T23))
permuteB_in_ga(.(T37, T38), .(T39, T40)) → U3_ga(T37, T38, T39, T40, deleteA_in_aga(T39, T38, X42))
deleteA_in_aga(T59, .(T59, T60), T60) → deleteA_out_aga(T59, .(T59, T60), T60)
deleteA_in_aga(T70, .(T68, T69), .(T68, X75)) → U1_aga(T70, T68, T69, X75, deleteA_in_aga(T70, T69, X75))
U1_aga(T70, T68, T69, X75, deleteA_out_aga(T70, T69, X75)) → deleteA_out_aga(T70, .(T68, T69), .(T68, X75))
U3_ga(T37, T38, T39, T40, deleteA_out_aga(T39, T38, X42)) → permuteB_out_ga(.(T37, T38), .(T39, T40))
permuteB_in_ga(.(T37, T38), .(T39, T46)) → U4_ga(T37, T38, T39, T46, deleteA_in_aga(T39, T38, T45))
U4_ga(T37, T38, T39, T46, deleteA_out_aga(T39, T38, T45)) → U5_ga(T37, T38, T39, T46, permuteB_in_ga(.(T37, T45), T46))
U5_ga(T37, T38, T39, T46, permuteB_out_ga(.(T37, T45), T46)) → permuteB_out_ga(.(T37, T38), .(T39, T46))
U2_ga(T21, T22, T23, permuteB_out_ga(T22, T23)) → permuteB_out_ga(.(T21, T22), .(T21, T23))
PERMUTEB_IN_GA(.(T37, T38), .(T39, T46)) → U4_GA(T37, T38, T39, T46, deleteA_in_aga(T39, T38, T45))
U4_GA(T37, T38, T39, T46, deleteA_out_aga(T39, T38, T45)) → PERMUTEB_IN_GA(.(T37, T45), T46)
PERMUTEB_IN_GA(.(T21, T22), .(T21, T23)) → PERMUTEB_IN_GA(T22, T23)
deleteA_in_aga(T59, .(T59, T60), T60) → deleteA_out_aga(T59, .(T59, T60), T60)
deleteA_in_aga(T70, .(T68, T69), .(T68, X75)) → U1_aga(T70, T68, T69, X75, deleteA_in_aga(T70, T69, X75))
U1_aga(T70, T68, T69, X75, deleteA_out_aga(T70, T69, X75)) → deleteA_out_aga(T70, .(T68, T69), .(T68, X75))
PERMUTEB_IN_GA(.(T37, T38)) → U4_GA(T37, deleteA_in_aga(T38))
U4_GA(T37, deleteA_out_aga(T39, T45)) → PERMUTEB_IN_GA(.(T37, T45))
PERMUTEB_IN_GA(.(T21, T22)) → PERMUTEB_IN_GA(T22)
deleteA_in_aga(.(T59, T60)) → deleteA_out_aga(T59, T60)
deleteA_in_aga(.(T68, T69)) → U1_aga(T68, deleteA_in_aga(T69))
U1_aga(T68, deleteA_out_aga(T70, X75)) → deleteA_out_aga(T70, .(T68, X75))
deleteA_in_aga(x0)
U1_aga(x0, x1)
PERMUTEB_IN_GA(.(T37, T38)) → U4_GA(T37, deleteA_in_aga(T38))
U4_GA(T37, deleteA_out_aga(T39, T45)) → PERMUTEB_IN_GA(.(T37, T45))
PERMUTEB_IN_GA(.(T21, T22)) → PERMUTEB_IN_GA(T22)
deleteA_in_aga(.(T59, T60)) → deleteA_out_aga(T59, T60)
deleteA_in_aga(.(T68, T69)) → U1_aga(T68, deleteA_in_aga(T69))
U1_aga(T68, deleteA_out_aga(T70, X75)) → deleteA_out_aga(T70, .(T68, X75))
PERMUTEBINGA1 > U4GA2 > deleteAinaga1 > U1aga2 > deleteAoutaga2 > .2
deleteA_in_aga_1=1
PERMUTEB_IN_GA_1=1
._2=1
deleteA_out_aga_2=2
U1_aga_2=1
U4_GA_2=0
deleteA_in_aga(x0)
U1_aga(x0, x1)